COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		SOURCE SYNTAX
C00003 00003			Interpteter for source language
C00005 00004	Notes:
C00006 00005	Theorem
C00007 00006	Try it:
C00010 ENDMK
C⊗;
	SOURCE SYNTAX

  Concrete
exp	::= var | const | sum

sum	::= exp + exp


  Abstract
exp	::= var | const | sum

sum	::= struct[ arg1:exp; arg2:exp]





	OBJECT SYNTAX

  Concrete
prog	::= inst prog
	::= ε

inst	::= li | lo | st | ad

li	::= <LI int>

lo	::= <LO adr>

st	::= <ST adr>

ad	::= <AD adr>


adr	::= int




 Abstract
prog	::= seq[inst]

inst	::= li 
	::= lo 
	::= st 
	::= ad

li	::= struct[cnst:int]

lo	::= struct[loc:adr]

	......

adr	::= int

		Interpteter for source language

value[e:exp;xi:environ_s]int
 generic(e)
	[var]      => c(e,xi)
	[const]    => val(e)
	[sum(u,v)] => +(value_s(u,xi),value_s(v,xi))
 end;



		Interpreter for object language

outcome[p:prog;eta:environ_o]environ_o
 on(p;eta,λ[[i,y]step(i y)])

step[i:inst; eta:environ_o] environ_o
 generic(i)
	[li(c)]   => a(AC,c,eta)
	[lo(adr)] => a(AC,cc(adr,eta),eta)
	[st(adr)] => a(adr,cc(AC,eta),eta)
	[ad(adr)] => a(AC,cc(AC,eta),eta) + cc(adr,eta),eta)
end;



		Compiler

compile[e:exp;t:adr]prog
 generic(e)
	[var]      => lo(map(e)) 
	[const]    => li(val(e))
	[sum(u,v)] =>  prog(compile(u,t),
			    prog(st(t),
			         prog(compile(v,t+1),
			              ad(t))))
end;


Notes:
	3.1-3.7 of McCarthy Painter are consequences of  data structures.
	3.13 is also consequence.


Theorem

outcome(compile(e:exp,t:adr),load(xi):environ_o) 

	=(t)
		a(AC,value(e:exp,xi:environ_s)load(xi):environ_o)

where:
map(e:var)adr   such that cc(map(e)load(xi)) = c(e,xi)

Try it:

outcome(						;load(xi):environ_o)
	compile[e:exp;t:adr]prog
	 generic(e)
		[var]      => lo(map(e))) 
		[const]    => li(val(e))
		[sum(u,v)] =>  prog(compile(u,t),
				    prog(st(t),
 				         prog(compile(v,t+1)),
				              prog(ad(t))))
	end;


equals up to t

a(AC,					 	,load(xi):environ_o)
	      value[e:exp;xi:environ_s]int
		generic(e)
	 	  [var]      => c(e,xi)
		  [const]    => val(e)
		  [sum(u,v)] => +(value(u,xi),value(v,xi))
		end;


Proof is generic on e;

i. [const]
outcome(li(val(e)),load(xi))
	= outcome(ε,step(li(val(e)),load(xi))
	= step(li(val(e)),load(xi))
	= a(AC,val(e),load(xi))


ii. [var]
outcome(lo(map(e)),load(xi))
	= outcome(ε,step(lo(map(e),load(xi)),load(xi))
	= step(lo(map(e)),load(xi))
	= a(AC,cc(map(e),load(xi)),load(xi))
	= a(AC,c(e,load(xi)),load(xi))



iii.
[sum(u,v)]
outcome( prog(compile(u,t),             ,load(xi))
  	      prog(st(t),
	           prog(compile(v,t+l)),
	                prog(ad(t))))
        )

	=

outcome(ad(t),
        outcome(compile(v,t+1)),
                outcome(st(t),
                        outcome(compile(u,t),load(xi)))))

But by induction:

outcome(compile(u,t),load(xi))))) =(t)  a(AC,value(u),load(xi)))))

So:

outcome(st(t)(
	      outcome(compile(u,t),load(xi))))) )
=

outcome(st(t)(
	       a(AC,value(u),load(xi)))))    )


=
                step(st(t),
                     a(AC,value(u),load(xi)))))

=

a(t,
  cc(AC,
     a(AC,value(u),load(xi)))
  a(AC,value(u),load(xi)))))

=(t+1)

a(t,
  cc(AC,
     a(AC,value(u),load(xi)))
  a(AC,value(u),load(xi)))))

=(t+1,AC)

a(t,
  cc(AC,
     a(AC,value(u),load(xi)))
  a(AC,value(u),load(xi)))))